Thực đơn
Luận lý Hoare Ví dụExample 1 | |||
{ x + 1 = 43 } {\displaystyle \{x+1=43\}\!} | y := x + 1 {\displaystyle \ y:=x+1\ \!} | { y = 43 } {\displaystyle \{y=43\}\!} | (Tiên đề gán) |
( x + 1 = 43 ⟹ x = 42 ) {\displaystyle (x+1=43\implies x=42)} | |||
{ x = 42 } {\displaystyle \{x=42\}\!} | y := x + 1 {\displaystyle \ y:=x+1\ \!} | { y = 43 ∧ x = 42 } {\displaystyle \{y=43\land x=42\}\!} | (Luật hệ quả) |
Example 2 | |||
{ x + 1 ≤ N } {\displaystyle \{x+1\leq N\}\!} | x := x + 1 {\displaystyle \ x:=x+1\ \!} | { x ≤ N } {\displaystyle \{x\leq N\}\ \!} | (Tiên đề gán) |
( x < N ⟹ x + 1 ≤ N {\displaystyle x<N\implies x+1\leq N} với x, N là kiểu số nguyên.) | |||
{ x < N } {\displaystyle \{x<N\}\!} | x := x + 1 {\displaystyle \ x:=x+1\ \!} | { x ≤ N } {\displaystyle \{x\leq N\}\ \!} | (Luật hệ quả) |
Thực đơn
Luận lý Hoare Ví dụLiên quan
Luận tội Luận tội Donald Trump lần thứ hai Luận tạng Luận tội tại Hoa Kỳ Luận thuyết trung tâm Luận lý Hoare Luận ngữ Luận cứ Luận văn Luận điểm SiriTài liệu tham khảo
WikiPedia: Luận lý Hoare http://www.cs.queensu.ca/home/specsoft/ http://j-algo.binaervarianz.de/index.php?language=... http://isabelle.in.tum.de/Bali/ http://www.spatial.maine.edu/~worboys/processes/ho... //dx.doi.org/10.1145%2F363235.363259 http://www.key-project.org/download/hoare/